x1:Realizer. (Rpre?(x1))  (Rpre-p(x1)  FinProbSpace) 

latex

Definitions	if b then t else f fi , tt, ff, Rpre-p(x1), t  T, Rpre?(x1), b, P  Q, x:A. B(x), False, Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, , Rnone(),
Lemmas	Rpre? wf, assert wf, true wf, false wf, es realizer wf